0 Prolog
↳1 PrologToDTProblemTransformerProof (⇒, 84 ms)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇒, 114 ms)
↳4 PiDP
↳5 DependencyGraphProof (⇔, 0 ms)
↳6 AND
↳7 PiDP
↳8 UsableRulesProof (⇔, 0 ms)
↳9 PiDP
↳10 PiDPToQDPProof (⇒, 0 ms)
↳11 QDP
↳12 QDPSizeChangeProof (⇔, 0 ms)
↳13 YES
↳14 PiDP
↳15 UsableRulesProof (⇔, 0 ms)
↳16 PiDP
↳17 PiDPToQDPProof (⇒, 0 ms)
↳18 QDP
↳19 QDPSizeChangeProof (⇔, 0 ms)
↳20 YES
↳21 PiDP
↳22 PiDPToQDPProof (⇒, 0 ms)
↳23 QDP
↳24 Rewriting (⇔, 0 ms)
↳25 QDP
↳26 UsableRulesProof (⇔, 0 ms)
↳27 QDP
↳28 QReductionProof (⇔, 0 ms)
↳29 QDP
↳30 Rewriting (⇔, 0 ms)
↳31 QDP
↳32 UsableRulesProof (⇔, 0 ms)
↳33 QDP
↳34 QReductionProof (⇔, 0 ms)
↳35 QDP
↳36 Instantiation (⇔, 0 ms)
↳37 QDP
↳38 QDPOrderProof (⇔, 126 ms)
↳39 QDP
↳40 DependencyGraphProof (⇔, 0 ms)
↳41 TRUE
PERMA_IN_GA(.(X1, X2), .(X1, X3)) → U3_GA(X1, X2, X3, append1cB_in_ga(X2, X4))
U3_GA(X1, X2, X3, append1cB_out_ga(X2, X4)) → U4_GA(X1, X2, X3, permA_in_ga(X4, X3))
U3_GA(X1, X2, X3, append1cB_out_ga(X2, X4)) → PERMA_IN_GA(X4, X3)
PERMA_IN_GA(.(X1, X2), .(X3, X4)) → U5_GA(X1, X2, X3, X4, append2C_in_aaag(X5, X3, X6, X2))
PERMA_IN_GA(.(X1, X2), .(X3, X4)) → APPEND2C_IN_AAAG(X5, X3, X6, X2)
APPEND2C_IN_AAAG(.(X1, X2), X3, X4, .(X1, X5)) → U1_AAAG(X1, X2, X3, X4, X5, append2C_in_aaag(X2, X3, X4, X5))
APPEND2C_IN_AAAG(.(X1, X2), X3, X4, .(X1, X5)) → APPEND2C_IN_AAAG(X2, X3, X4, X5)
PERMA_IN_GA(.(X1, X2), .(X3, X4)) → U6_GA(X1, X2, X3, X4, append2cC_in_aaag(X5, X3, X6, X2))
U6_GA(X1, X2, X3, X4, append2cC_out_aaag(X5, X3, X6, X2)) → U7_GA(X1, X2, X3, X4, append1E_in_gga(X5, X6, X7))
U6_GA(X1, X2, X3, X4, append2cC_out_aaag(X5, X3, X6, X2)) → APPEND1E_IN_GGA(X5, X6, X7)
APPEND1E_IN_GGA(.(X1, X2), X3, .(X1, X4)) → U2_GGA(X1, X2, X3, X4, append1E_in_gga(X2, X3, X4))
APPEND1E_IN_GGA(.(X1, X2), X3, .(X1, X4)) → APPEND1E_IN_GGA(X2, X3, X4)
U6_GA(X1, X2, X3, X4, append2cC_out_aaag(X5, X3, X6, X2)) → U8_GA(X1, X2, X3, X4, append1cD_in_ggga(X1, X5, X6, X7))
U8_GA(X1, X2, X3, X4, append1cD_out_ggga(X1, X5, X6, X7)) → U9_GA(X1, X2, X3, X4, permA_in_ga(X7, X4))
U8_GA(X1, X2, X3, X4, append1cD_out_ggga(X1, X5, X6, X7)) → PERMA_IN_GA(X7, X4)
append1cB_in_ga(X1, X1) → append1cB_out_ga(X1, X1)
append2cC_in_aaag([], X1, X2, .(X1, X2)) → append2cC_out_aaag([], X1, X2, .(X1, X2))
append2cC_in_aaag(.(X1, X2), X3, X4, .(X1, X5)) → U16_aaag(X1, X2, X3, X4, X5, append2cC_in_aaag(X2, X3, X4, X5))
U16_aaag(X1, X2, X3, X4, X5, append2cC_out_aaag(X2, X3, X4, X5)) → append2cC_out_aaag(.(X1, X2), X3, X4, .(X1, X5))
append1cD_in_ggga(X1, X2, X3, .(X1, X4)) → U18_ggga(X1, X2, X3, X4, append1cE_in_gga(X2, X3, X4))
append1cE_in_gga([], X1, X1) → append1cE_out_gga([], X1, X1)
append1cE_in_gga(.(X1, X2), X3, .(X1, X4)) → U17_gga(X1, X2, X3, X4, append1cE_in_gga(X2, X3, X4))
U17_gga(X1, X2, X3, X4, append1cE_out_gga(X2, X3, X4)) → append1cE_out_gga(.(X1, X2), X3, .(X1, X4))
U18_ggga(X1, X2, X3, X4, append1cE_out_gga(X2, X3, X4)) → append1cD_out_ggga(X1, X2, X3, .(X1, X4))
Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES
PERMA_IN_GA(.(X1, X2), .(X1, X3)) → U3_GA(X1, X2, X3, append1cB_in_ga(X2, X4))
U3_GA(X1, X2, X3, append1cB_out_ga(X2, X4)) → U4_GA(X1, X2, X3, permA_in_ga(X4, X3))
U3_GA(X1, X2, X3, append1cB_out_ga(X2, X4)) → PERMA_IN_GA(X4, X3)
PERMA_IN_GA(.(X1, X2), .(X3, X4)) → U5_GA(X1, X2, X3, X4, append2C_in_aaag(X5, X3, X6, X2))
PERMA_IN_GA(.(X1, X2), .(X3, X4)) → APPEND2C_IN_AAAG(X5, X3, X6, X2)
APPEND2C_IN_AAAG(.(X1, X2), X3, X4, .(X1, X5)) → U1_AAAG(X1, X2, X3, X4, X5, append2C_in_aaag(X2, X3, X4, X5))
APPEND2C_IN_AAAG(.(X1, X2), X3, X4, .(X1, X5)) → APPEND2C_IN_AAAG(X2, X3, X4, X5)
PERMA_IN_GA(.(X1, X2), .(X3, X4)) → U6_GA(X1, X2, X3, X4, append2cC_in_aaag(X5, X3, X6, X2))
U6_GA(X1, X2, X3, X4, append2cC_out_aaag(X5, X3, X6, X2)) → U7_GA(X1, X2, X3, X4, append1E_in_gga(X5, X6, X7))
U6_GA(X1, X2, X3, X4, append2cC_out_aaag(X5, X3, X6, X2)) → APPEND1E_IN_GGA(X5, X6, X7)
APPEND1E_IN_GGA(.(X1, X2), X3, .(X1, X4)) → U2_GGA(X1, X2, X3, X4, append1E_in_gga(X2, X3, X4))
APPEND1E_IN_GGA(.(X1, X2), X3, .(X1, X4)) → APPEND1E_IN_GGA(X2, X3, X4)
U6_GA(X1, X2, X3, X4, append2cC_out_aaag(X5, X3, X6, X2)) → U8_GA(X1, X2, X3, X4, append1cD_in_ggga(X1, X5, X6, X7))
U8_GA(X1, X2, X3, X4, append1cD_out_ggga(X1, X5, X6, X7)) → U9_GA(X1, X2, X3, X4, permA_in_ga(X7, X4))
U8_GA(X1, X2, X3, X4, append1cD_out_ggga(X1, X5, X6, X7)) → PERMA_IN_GA(X7, X4)
append1cB_in_ga(X1, X1) → append1cB_out_ga(X1, X1)
append2cC_in_aaag([], X1, X2, .(X1, X2)) → append2cC_out_aaag([], X1, X2, .(X1, X2))
append2cC_in_aaag(.(X1, X2), X3, X4, .(X1, X5)) → U16_aaag(X1, X2, X3, X4, X5, append2cC_in_aaag(X2, X3, X4, X5))
U16_aaag(X1, X2, X3, X4, X5, append2cC_out_aaag(X2, X3, X4, X5)) → append2cC_out_aaag(.(X1, X2), X3, X4, .(X1, X5))
append1cD_in_ggga(X1, X2, X3, .(X1, X4)) → U18_ggga(X1, X2, X3, X4, append1cE_in_gga(X2, X3, X4))
append1cE_in_gga([], X1, X1) → append1cE_out_gga([], X1, X1)
append1cE_in_gga(.(X1, X2), X3, .(X1, X4)) → U17_gga(X1, X2, X3, X4, append1cE_in_gga(X2, X3, X4))
U17_gga(X1, X2, X3, X4, append1cE_out_gga(X2, X3, X4)) → append1cE_out_gga(.(X1, X2), X3, .(X1, X4))
U18_ggga(X1, X2, X3, X4, append1cE_out_gga(X2, X3, X4)) → append1cD_out_ggga(X1, X2, X3, .(X1, X4))
APPEND1E_IN_GGA(.(X1, X2), X3, .(X1, X4)) → APPEND1E_IN_GGA(X2, X3, X4)
append1cB_in_ga(X1, X1) → append1cB_out_ga(X1, X1)
append2cC_in_aaag([], X1, X2, .(X1, X2)) → append2cC_out_aaag([], X1, X2, .(X1, X2))
append2cC_in_aaag(.(X1, X2), X3, X4, .(X1, X5)) → U16_aaag(X1, X2, X3, X4, X5, append2cC_in_aaag(X2, X3, X4, X5))
U16_aaag(X1, X2, X3, X4, X5, append2cC_out_aaag(X2, X3, X4, X5)) → append2cC_out_aaag(.(X1, X2), X3, X4, .(X1, X5))
append1cD_in_ggga(X1, X2, X3, .(X1, X4)) → U18_ggga(X1, X2, X3, X4, append1cE_in_gga(X2, X3, X4))
append1cE_in_gga([], X1, X1) → append1cE_out_gga([], X1, X1)
append1cE_in_gga(.(X1, X2), X3, .(X1, X4)) → U17_gga(X1, X2, X3, X4, append1cE_in_gga(X2, X3, X4))
U17_gga(X1, X2, X3, X4, append1cE_out_gga(X2, X3, X4)) → append1cE_out_gga(.(X1, X2), X3, .(X1, X4))
U18_ggga(X1, X2, X3, X4, append1cE_out_gga(X2, X3, X4)) → append1cD_out_ggga(X1, X2, X3, .(X1, X4))
APPEND1E_IN_GGA(.(X1, X2), X3, .(X1, X4)) → APPEND1E_IN_GGA(X2, X3, X4)
APPEND1E_IN_GGA(.(X1, X2), X3) → APPEND1E_IN_GGA(X2, X3)
From the DPs we obtained the following set of size-change graphs:
APPEND2C_IN_AAAG(.(X1, X2), X3, X4, .(X1, X5)) → APPEND2C_IN_AAAG(X2, X3, X4, X5)
append1cB_in_ga(X1, X1) → append1cB_out_ga(X1, X1)
append2cC_in_aaag([], X1, X2, .(X1, X2)) → append2cC_out_aaag([], X1, X2, .(X1, X2))
append2cC_in_aaag(.(X1, X2), X3, X4, .(X1, X5)) → U16_aaag(X1, X2, X3, X4, X5, append2cC_in_aaag(X2, X3, X4, X5))
U16_aaag(X1, X2, X3, X4, X5, append2cC_out_aaag(X2, X3, X4, X5)) → append2cC_out_aaag(.(X1, X2), X3, X4, .(X1, X5))
append1cD_in_ggga(X1, X2, X3, .(X1, X4)) → U18_ggga(X1, X2, X3, X4, append1cE_in_gga(X2, X3, X4))
append1cE_in_gga([], X1, X1) → append1cE_out_gga([], X1, X1)
append1cE_in_gga(.(X1, X2), X3, .(X1, X4)) → U17_gga(X1, X2, X3, X4, append1cE_in_gga(X2, X3, X4))
U17_gga(X1, X2, X3, X4, append1cE_out_gga(X2, X3, X4)) → append1cE_out_gga(.(X1, X2), X3, .(X1, X4))
U18_ggga(X1, X2, X3, X4, append1cE_out_gga(X2, X3, X4)) → append1cD_out_ggga(X1, X2, X3, .(X1, X4))
APPEND2C_IN_AAAG(.(X1, X2), X3, X4, .(X1, X5)) → APPEND2C_IN_AAAG(X2, X3, X4, X5)
APPEND2C_IN_AAAG(.(X1, X5)) → APPEND2C_IN_AAAG(X5)
From the DPs we obtained the following set of size-change graphs:
U3_GA(X1, X2, X3, append1cB_out_ga(X2, X4)) → PERMA_IN_GA(X4, X3)
PERMA_IN_GA(.(X1, X2), .(X1, X3)) → U3_GA(X1, X2, X3, append1cB_in_ga(X2, X4))
PERMA_IN_GA(.(X1, X2), .(X3, X4)) → U6_GA(X1, X2, X3, X4, append2cC_in_aaag(X5, X3, X6, X2))
U6_GA(X1, X2, X3, X4, append2cC_out_aaag(X5, X3, X6, X2)) → U8_GA(X1, X2, X3, X4, append1cD_in_ggga(X1, X5, X6, X7))
U8_GA(X1, X2, X3, X4, append1cD_out_ggga(X1, X5, X6, X7)) → PERMA_IN_GA(X7, X4)
append1cB_in_ga(X1, X1) → append1cB_out_ga(X1, X1)
append2cC_in_aaag([], X1, X2, .(X1, X2)) → append2cC_out_aaag([], X1, X2, .(X1, X2))
append2cC_in_aaag(.(X1, X2), X3, X4, .(X1, X5)) → U16_aaag(X1, X2, X3, X4, X5, append2cC_in_aaag(X2, X3, X4, X5))
U16_aaag(X1, X2, X3, X4, X5, append2cC_out_aaag(X2, X3, X4, X5)) → append2cC_out_aaag(.(X1, X2), X3, X4, .(X1, X5))
append1cD_in_ggga(X1, X2, X3, .(X1, X4)) → U18_ggga(X1, X2, X3, X4, append1cE_in_gga(X2, X3, X4))
append1cE_in_gga([], X1, X1) → append1cE_out_gga([], X1, X1)
append1cE_in_gga(.(X1, X2), X3, .(X1, X4)) → U17_gga(X1, X2, X3, X4, append1cE_in_gga(X2, X3, X4))
U17_gga(X1, X2, X3, X4, append1cE_out_gga(X2, X3, X4)) → append1cE_out_gga(.(X1, X2), X3, .(X1, X4))
U18_ggga(X1, X2, X3, X4, append1cE_out_gga(X2, X3, X4)) → append1cD_out_ggga(X1, X2, X3, .(X1, X4))
U3_GA(X1, X2, append1cB_out_ga(X2, X4)) → PERMA_IN_GA(X4)
PERMA_IN_GA(.(X1, X2)) → U3_GA(X1, X2, append1cB_in_ga(X2))
PERMA_IN_GA(.(X1, X2)) → U6_GA(X1, X2, append2cC_in_aaag(X2))
U6_GA(X1, X2, append2cC_out_aaag(X5, X3, X6, X2)) → U8_GA(X1, X2, append1cD_in_ggga(X1, X5, X6))
U8_GA(X1, X2, append1cD_out_ggga(X1, X5, X6, X7)) → PERMA_IN_GA(X7)
append1cB_in_ga(X1) → append1cB_out_ga(X1, X1)
append2cC_in_aaag(.(X1, X2)) → append2cC_out_aaag([], X1, X2, .(X1, X2))
append2cC_in_aaag(.(X1, X5)) → U16_aaag(X1, X5, append2cC_in_aaag(X5))
U16_aaag(X1, X5, append2cC_out_aaag(X2, X3, X4, X5)) → append2cC_out_aaag(.(X1, X2), X3, X4, .(X1, X5))
append1cD_in_ggga(X1, X2, X3) → U18_ggga(X1, X2, X3, append1cE_in_gga(X2, X3))
append1cE_in_gga([], X1) → append1cE_out_gga([], X1, X1)
append1cE_in_gga(.(X1, X2), X3) → U17_gga(X1, X2, X3, append1cE_in_gga(X2, X3))
U17_gga(X1, X2, X3, append1cE_out_gga(X2, X3, X4)) → append1cE_out_gga(.(X1, X2), X3, .(X1, X4))
U18_ggga(X1, X2, X3, append1cE_out_gga(X2, X3, X4)) → append1cD_out_ggga(X1, X2, X3, .(X1, X4))
append1cB_in_ga(x0)
append2cC_in_aaag(x0)
U16_aaag(x0, x1, x2)
append1cD_in_ggga(x0, x1, x2)
append1cE_in_gga(x0, x1)
U17_gga(x0, x1, x2, x3)
U18_ggga(x0, x1, x2, x3)
PERMA_IN_GA(.(X1, X2)) → U3_GA(X1, X2, append1cB_out_ga(X2, X2))
U3_GA(X1, X2, append1cB_out_ga(X2, X4)) → PERMA_IN_GA(X4)
PERMA_IN_GA(.(X1, X2)) → U6_GA(X1, X2, append2cC_in_aaag(X2))
U6_GA(X1, X2, append2cC_out_aaag(X5, X3, X6, X2)) → U8_GA(X1, X2, append1cD_in_ggga(X1, X5, X6))
U8_GA(X1, X2, append1cD_out_ggga(X1, X5, X6, X7)) → PERMA_IN_GA(X7)
PERMA_IN_GA(.(X1, X2)) → U3_GA(X1, X2, append1cB_out_ga(X2, X2))
append1cB_in_ga(X1) → append1cB_out_ga(X1, X1)
append2cC_in_aaag(.(X1, X2)) → append2cC_out_aaag([], X1, X2, .(X1, X2))
append2cC_in_aaag(.(X1, X5)) → U16_aaag(X1, X5, append2cC_in_aaag(X5))
U16_aaag(X1, X5, append2cC_out_aaag(X2, X3, X4, X5)) → append2cC_out_aaag(.(X1, X2), X3, X4, .(X1, X5))
append1cD_in_ggga(X1, X2, X3) → U18_ggga(X1, X2, X3, append1cE_in_gga(X2, X3))
append1cE_in_gga([], X1) → append1cE_out_gga([], X1, X1)
append1cE_in_gga(.(X1, X2), X3) → U17_gga(X1, X2, X3, append1cE_in_gga(X2, X3))
U17_gga(X1, X2, X3, append1cE_out_gga(X2, X3, X4)) → append1cE_out_gga(.(X1, X2), X3, .(X1, X4))
U18_ggga(X1, X2, X3, append1cE_out_gga(X2, X3, X4)) → append1cD_out_ggga(X1, X2, X3, .(X1, X4))
append1cB_in_ga(x0)
append2cC_in_aaag(x0)
U16_aaag(x0, x1, x2)
append1cD_in_ggga(x0, x1, x2)
append1cE_in_gga(x0, x1)
U17_gga(x0, x1, x2, x3)
U18_ggga(x0, x1, x2, x3)
U3_GA(X1, X2, append1cB_out_ga(X2, X4)) → PERMA_IN_GA(X4)
PERMA_IN_GA(.(X1, X2)) → U6_GA(X1, X2, append2cC_in_aaag(X2))
U6_GA(X1, X2, append2cC_out_aaag(X5, X3, X6, X2)) → U8_GA(X1, X2, append1cD_in_ggga(X1, X5, X6))
U8_GA(X1, X2, append1cD_out_ggga(X1, X5, X6, X7)) → PERMA_IN_GA(X7)
PERMA_IN_GA(.(X1, X2)) → U3_GA(X1, X2, append1cB_out_ga(X2, X2))
append1cD_in_ggga(X1, X2, X3) → U18_ggga(X1, X2, X3, append1cE_in_gga(X2, X3))
append1cE_in_gga([], X1) → append1cE_out_gga([], X1, X1)
append1cE_in_gga(.(X1, X2), X3) → U17_gga(X1, X2, X3, append1cE_in_gga(X2, X3))
U18_ggga(X1, X2, X3, append1cE_out_gga(X2, X3, X4)) → append1cD_out_ggga(X1, X2, X3, .(X1, X4))
U17_gga(X1, X2, X3, append1cE_out_gga(X2, X3, X4)) → append1cE_out_gga(.(X1, X2), X3, .(X1, X4))
append2cC_in_aaag(.(X1, X2)) → append2cC_out_aaag([], X1, X2, .(X1, X2))
append2cC_in_aaag(.(X1, X5)) → U16_aaag(X1, X5, append2cC_in_aaag(X5))
U16_aaag(X1, X5, append2cC_out_aaag(X2, X3, X4, X5)) → append2cC_out_aaag(.(X1, X2), X3, X4, .(X1, X5))
append1cB_in_ga(x0)
append2cC_in_aaag(x0)
U16_aaag(x0, x1, x2)
append1cD_in_ggga(x0, x1, x2)
append1cE_in_gga(x0, x1)
U17_gga(x0, x1, x2, x3)
U18_ggga(x0, x1, x2, x3)
append1cB_in_ga(x0)
U3_GA(X1, X2, append1cB_out_ga(X2, X4)) → PERMA_IN_GA(X4)
PERMA_IN_GA(.(X1, X2)) → U6_GA(X1, X2, append2cC_in_aaag(X2))
U6_GA(X1, X2, append2cC_out_aaag(X5, X3, X6, X2)) → U8_GA(X1, X2, append1cD_in_ggga(X1, X5, X6))
U8_GA(X1, X2, append1cD_out_ggga(X1, X5, X6, X7)) → PERMA_IN_GA(X7)
PERMA_IN_GA(.(X1, X2)) → U3_GA(X1, X2, append1cB_out_ga(X2, X2))
append1cD_in_ggga(X1, X2, X3) → U18_ggga(X1, X2, X3, append1cE_in_gga(X2, X3))
append1cE_in_gga([], X1) → append1cE_out_gga([], X1, X1)
append1cE_in_gga(.(X1, X2), X3) → U17_gga(X1, X2, X3, append1cE_in_gga(X2, X3))
U18_ggga(X1, X2, X3, append1cE_out_gga(X2, X3, X4)) → append1cD_out_ggga(X1, X2, X3, .(X1, X4))
U17_gga(X1, X2, X3, append1cE_out_gga(X2, X3, X4)) → append1cE_out_gga(.(X1, X2), X3, .(X1, X4))
append2cC_in_aaag(.(X1, X2)) → append2cC_out_aaag([], X1, X2, .(X1, X2))
append2cC_in_aaag(.(X1, X5)) → U16_aaag(X1, X5, append2cC_in_aaag(X5))
U16_aaag(X1, X5, append2cC_out_aaag(X2, X3, X4, X5)) → append2cC_out_aaag(.(X1, X2), X3, X4, .(X1, X5))
append2cC_in_aaag(x0)
U16_aaag(x0, x1, x2)
append1cD_in_ggga(x0, x1, x2)
append1cE_in_gga(x0, x1)
U17_gga(x0, x1, x2, x3)
U18_ggga(x0, x1, x2, x3)
U6_GA(X1, X2, append2cC_out_aaag(X5, X3, X6, X2)) → U8_GA(X1, X2, U18_ggga(X1, X5, X6, append1cE_in_gga(X5, X6)))
U3_GA(X1, X2, append1cB_out_ga(X2, X4)) → PERMA_IN_GA(X4)
PERMA_IN_GA(.(X1, X2)) → U6_GA(X1, X2, append2cC_in_aaag(X2))
U8_GA(X1, X2, append1cD_out_ggga(X1, X5, X6, X7)) → PERMA_IN_GA(X7)
PERMA_IN_GA(.(X1, X2)) → U3_GA(X1, X2, append1cB_out_ga(X2, X2))
U6_GA(X1, X2, append2cC_out_aaag(X5, X3, X6, X2)) → U8_GA(X1, X2, U18_ggga(X1, X5, X6, append1cE_in_gga(X5, X6)))
append1cD_in_ggga(X1, X2, X3) → U18_ggga(X1, X2, X3, append1cE_in_gga(X2, X3))
append1cE_in_gga([], X1) → append1cE_out_gga([], X1, X1)
append1cE_in_gga(.(X1, X2), X3) → U17_gga(X1, X2, X3, append1cE_in_gga(X2, X3))
U18_ggga(X1, X2, X3, append1cE_out_gga(X2, X3, X4)) → append1cD_out_ggga(X1, X2, X3, .(X1, X4))
U17_gga(X1, X2, X3, append1cE_out_gga(X2, X3, X4)) → append1cE_out_gga(.(X1, X2), X3, .(X1, X4))
append2cC_in_aaag(.(X1, X2)) → append2cC_out_aaag([], X1, X2, .(X1, X2))
append2cC_in_aaag(.(X1, X5)) → U16_aaag(X1, X5, append2cC_in_aaag(X5))
U16_aaag(X1, X5, append2cC_out_aaag(X2, X3, X4, X5)) → append2cC_out_aaag(.(X1, X2), X3, X4, .(X1, X5))
append2cC_in_aaag(x0)
U16_aaag(x0, x1, x2)
append1cD_in_ggga(x0, x1, x2)
append1cE_in_gga(x0, x1)
U17_gga(x0, x1, x2, x3)
U18_ggga(x0, x1, x2, x3)
U3_GA(X1, X2, append1cB_out_ga(X2, X4)) → PERMA_IN_GA(X4)
PERMA_IN_GA(.(X1, X2)) → U6_GA(X1, X2, append2cC_in_aaag(X2))
U8_GA(X1, X2, append1cD_out_ggga(X1, X5, X6, X7)) → PERMA_IN_GA(X7)
PERMA_IN_GA(.(X1, X2)) → U3_GA(X1, X2, append1cB_out_ga(X2, X2))
U6_GA(X1, X2, append2cC_out_aaag(X5, X3, X6, X2)) → U8_GA(X1, X2, U18_ggga(X1, X5, X6, append1cE_in_gga(X5, X6)))
append1cE_in_gga([], X1) → append1cE_out_gga([], X1, X1)
append1cE_in_gga(.(X1, X2), X3) → U17_gga(X1, X2, X3, append1cE_in_gga(X2, X3))
U18_ggga(X1, X2, X3, append1cE_out_gga(X2, X3, X4)) → append1cD_out_ggga(X1, X2, X3, .(X1, X4))
U17_gga(X1, X2, X3, append1cE_out_gga(X2, X3, X4)) → append1cE_out_gga(.(X1, X2), X3, .(X1, X4))
append2cC_in_aaag(.(X1, X2)) → append2cC_out_aaag([], X1, X2, .(X1, X2))
append2cC_in_aaag(.(X1, X5)) → U16_aaag(X1, X5, append2cC_in_aaag(X5))
U16_aaag(X1, X5, append2cC_out_aaag(X2, X3, X4, X5)) → append2cC_out_aaag(.(X1, X2), X3, X4, .(X1, X5))
append2cC_in_aaag(x0)
U16_aaag(x0, x1, x2)
append1cD_in_ggga(x0, x1, x2)
append1cE_in_gga(x0, x1)
U17_gga(x0, x1, x2, x3)
U18_ggga(x0, x1, x2, x3)
append1cD_in_ggga(x0, x1, x2)
U3_GA(X1, X2, append1cB_out_ga(X2, X4)) → PERMA_IN_GA(X4)
PERMA_IN_GA(.(X1, X2)) → U6_GA(X1, X2, append2cC_in_aaag(X2))
U8_GA(X1, X2, append1cD_out_ggga(X1, X5, X6, X7)) → PERMA_IN_GA(X7)
PERMA_IN_GA(.(X1, X2)) → U3_GA(X1, X2, append1cB_out_ga(X2, X2))
U6_GA(X1, X2, append2cC_out_aaag(X5, X3, X6, X2)) → U8_GA(X1, X2, U18_ggga(X1, X5, X6, append1cE_in_gga(X5, X6)))
append1cE_in_gga([], X1) → append1cE_out_gga([], X1, X1)
append1cE_in_gga(.(X1, X2), X3) → U17_gga(X1, X2, X3, append1cE_in_gga(X2, X3))
U18_ggga(X1, X2, X3, append1cE_out_gga(X2, X3, X4)) → append1cD_out_ggga(X1, X2, X3, .(X1, X4))
U17_gga(X1, X2, X3, append1cE_out_gga(X2, X3, X4)) → append1cE_out_gga(.(X1, X2), X3, .(X1, X4))
append2cC_in_aaag(.(X1, X2)) → append2cC_out_aaag([], X1, X2, .(X1, X2))
append2cC_in_aaag(.(X1, X5)) → U16_aaag(X1, X5, append2cC_in_aaag(X5))
U16_aaag(X1, X5, append2cC_out_aaag(X2, X3, X4, X5)) → append2cC_out_aaag(.(X1, X2), X3, X4, .(X1, X5))
append2cC_in_aaag(x0)
U16_aaag(x0, x1, x2)
append1cE_in_gga(x0, x1)
U17_gga(x0, x1, x2, x3)
U18_ggga(x0, x1, x2, x3)
U3_GA(z0, z1, append1cB_out_ga(z1, z1)) → PERMA_IN_GA(z1)
PERMA_IN_GA(.(X1, X2)) → U6_GA(X1, X2, append2cC_in_aaag(X2))
U8_GA(X1, X2, append1cD_out_ggga(X1, X5, X6, X7)) → PERMA_IN_GA(X7)
PERMA_IN_GA(.(X1, X2)) → U3_GA(X1, X2, append1cB_out_ga(X2, X2))
U6_GA(X1, X2, append2cC_out_aaag(X5, X3, X6, X2)) → U8_GA(X1, X2, U18_ggga(X1, X5, X6, append1cE_in_gga(X5, X6)))
U3_GA(z0, z1, append1cB_out_ga(z1, z1)) → PERMA_IN_GA(z1)
append1cE_in_gga([], X1) → append1cE_out_gga([], X1, X1)
append1cE_in_gga(.(X1, X2), X3) → U17_gga(X1, X2, X3, append1cE_in_gga(X2, X3))
U18_ggga(X1, X2, X3, append1cE_out_gga(X2, X3, X4)) → append1cD_out_ggga(X1, X2, X3, .(X1, X4))
U17_gga(X1, X2, X3, append1cE_out_gga(X2, X3, X4)) → append1cE_out_gga(.(X1, X2), X3, .(X1, X4))
append2cC_in_aaag(.(X1, X2)) → append2cC_out_aaag([], X1, X2, .(X1, X2))
append2cC_in_aaag(.(X1, X5)) → U16_aaag(X1, X5, append2cC_in_aaag(X5))
U16_aaag(X1, X5, append2cC_out_aaag(X2, X3, X4, X5)) → append2cC_out_aaag(.(X1, X2), X3, X4, .(X1, X5))
append2cC_in_aaag(x0)
U16_aaag(x0, x1, x2)
append1cE_in_gga(x0, x1)
U17_gga(x0, x1, x2, x3)
U18_ggga(x0, x1, x2, x3)
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
U6_GA(X1, X2, append2cC_out_aaag(X5, X3, X6, X2)) → U8_GA(X1, X2, U18_ggga(X1, X5, X6, append1cE_in_gga(X5, X6)))
U3_GA(z0, z1, append1cB_out_ga(z1, z1)) → PERMA_IN_GA(z1)
POL(.(x1, x2)) = 1 + x2
POL(PERMA_IN_GA(x1)) = x1
POL(U16_aaag(x1, x2, x3)) = 1 + x3
POL(U17_gga(x1, x2, x3, x4)) = 1 + x4
POL(U18_ggga(x1, x2, x3, x4)) = x4
POL(U3_GA(x1, x2, x3)) = x2 + x3
POL(U6_GA(x1, x2, x3)) = 1 + x3
POL(U8_GA(x1, x2, x3)) = x3
POL([]) = 0
POL(append1cB_out_ga(x1, x2)) = 1
POL(append1cD_out_ggga(x1, x2, x3, x4)) = x4
POL(append1cE_in_gga(x1, x2)) = 1 + x1 + x2
POL(append1cE_out_gga(x1, x2, x3)) = 1 + x3
POL(append2cC_in_aaag(x1)) = x1
POL(append2cC_out_aaag(x1, x2, x3, x4)) = 1 + x1 + x3
append2cC_in_aaag(.(X1, X2)) → append2cC_out_aaag([], X1, X2, .(X1, X2))
append2cC_in_aaag(.(X1, X5)) → U16_aaag(X1, X5, append2cC_in_aaag(X5))
append1cE_in_gga([], X1) → append1cE_out_gga([], X1, X1)
append1cE_in_gga(.(X1, X2), X3) → U17_gga(X1, X2, X3, append1cE_in_gga(X2, X3))
U18_ggga(X1, X2, X3, append1cE_out_gga(X2, X3, X4)) → append1cD_out_ggga(X1, X2, X3, .(X1, X4))
U17_gga(X1, X2, X3, append1cE_out_gga(X2, X3, X4)) → append1cE_out_gga(.(X1, X2), X3, .(X1, X4))
U16_aaag(X1, X5, append2cC_out_aaag(X2, X3, X4, X5)) → append2cC_out_aaag(.(X1, X2), X3, X4, .(X1, X5))
PERMA_IN_GA(.(X1, X2)) → U6_GA(X1, X2, append2cC_in_aaag(X2))
U8_GA(X1, X2, append1cD_out_ggga(X1, X5, X6, X7)) → PERMA_IN_GA(X7)
PERMA_IN_GA(.(X1, X2)) → U3_GA(X1, X2, append1cB_out_ga(X2, X2))
append1cE_in_gga([], X1) → append1cE_out_gga([], X1, X1)
append1cE_in_gga(.(X1, X2), X3) → U17_gga(X1, X2, X3, append1cE_in_gga(X2, X3))
U18_ggga(X1, X2, X3, append1cE_out_gga(X2, X3, X4)) → append1cD_out_ggga(X1, X2, X3, .(X1, X4))
U17_gga(X1, X2, X3, append1cE_out_gga(X2, X3, X4)) → append1cE_out_gga(.(X1, X2), X3, .(X1, X4))
append2cC_in_aaag(.(X1, X2)) → append2cC_out_aaag([], X1, X2, .(X1, X2))
append2cC_in_aaag(.(X1, X5)) → U16_aaag(X1, X5, append2cC_in_aaag(X5))
U16_aaag(X1, X5, append2cC_out_aaag(X2, X3, X4, X5)) → append2cC_out_aaag(.(X1, X2), X3, X4, .(X1, X5))
append2cC_in_aaag(x0)
U16_aaag(x0, x1, x2)
append1cE_in_gga(x0, x1)
U17_gga(x0, x1, x2, x3)
U18_ggga(x0, x1, x2, x3)